Inference at * 2 1 1 0 
Iof proof for Lemma select nth tl:



1. T : Type
2. T List
3. u : T
4. v : T List
5. n:{0...||v||}, i:{0..(||v|| - n)}. nth_tl(n;v)[i] = v[(i+n)]
6. n : {0...||v||+1}
7. i : {0..((||v||+1) - n)}
8. n  0
9. n = 0
  [u / v][i] = [u / v][(i+n)] 

latex

 by PERMUTE{1:n, 2:n, 1:n, 3:n, 4:n, 5:n, 4:n, 6:n, 7:n, 8:n, 9:n} 

latex

 1: .....wf..... NILNIL

 1:   T = T
 2: .....wf..... NILNIL

 2:   [u / v][i] = [u / v][i]
 3: .....wf..... NILNIL

 3:   [u / v] = [u / v]
 4: .....wf..... NILNIL

 4:   i  
 5: .....wf..... NILNIL

 5:   n  
 6: .....wf..... NILNIL

 6:   0  
 7: 

 7:   i = i
 8: .....antecedent..... NILNIL

 8:   (0  (i+n)) & ((i+n) < ||[u / v]||)
 9: 

 9:   [u / v][i] = [u / v][(i+0)]
 .

Definitions	x:A  B(x), {x:A| B(x)} , a < b, x:AB(x), Ax, x.A(x), f(a), [car / cdr], , A  B, n+m, nth_tl(n;as), l[i], s = t, n - m, {i..j}, ||as||, #$n, {i...j}, type List, Type, x:A. B(x), , P  Q, True, t  T, P & Q, T, P  Q, P  Q
Lemmas	add functionality wrt eq, length wf1, le wf, squash wf, select wf